Broadly speaking, programming languages are divided into functional style programming languages and imperative style programming languages. Examples of imperative style programming languages are Java versions 1-7, C, C++, and C #. Examples of functional style programming languages are Lisp, meta language (ML), objective Caml (OCaml), Haskell, and F #. Some recent programming languages such as Java 8 incorporate both imperative programming features and functional programming features.
Often it is difficult to verify whether software will perform the tasks that it was designed to perform. Accordingly, specifications are commonly written that specify what a piece of software is supposed to do. Such specifications may be written in a manner that is machine interpretable by deductive verification (DV) (also called static verification) tools. A DV tool interprets a specification and program code, and then determines whether the program code operates in the manner prescribed by the specification.